1. $T$ : Type
\\[0ex]2. $x$ : $T$
\\[0ex]3. $y$ : $T$
\\[0ex]4. $u$ : $T$
\\[0ex]5. $L$ : $T$ List
\\[0ex]6. 0 $<$ $\parallel$$L$$\parallel$
\\[0ex]7. ($x$ = $u$ \& $y$ = hd($L$)) $\vee$ ($\exists$$i$:\{0..($\parallel$$L$$\parallel$ {-} 1)$^{-}$\}. ($x$ = $L$[$i$] \& $y$ = $L$[($i$+1)]))
\\[0ex]$\vdash$  $\exists$$i$:\{0..(($\parallel$$L$$\parallel$+1) {-} 1)$^{-}$\}. ($x$ = [$u$ / $L$][$i$] \& $y$ = [$u$ / $L$][($i$+1)])